T:Type, eq, le:(TT), op:(TTT), id:T, inv:(TT).
Assoc(T;op)  Ident(T;op;id)  (<T, eq, le, op, id, inv>  IMonoid) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), GrpSig, |g|, *, e, IMonoid
Definitions	t  T, P  Q, x:A. B(x), IMonoid, GrpSig, t.2, t.1, e, *, |g|, P & Q, IsMonoid(T;op;id),
Lemmas	bool wf, assoc wf, ident wf, grp id wf, grp op wf, grp car wf, monoid p wf